Termination w.r.t. Q proof of TRS/secret05cime2.trs

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

circ₂(cons₂(a, s), t) -> cons₂(msubst₂(a, t), circ₂(s, t))
circ₂(cons₂(lift, s), cons₂(a, t)) -> cons₂(a, circ₂(s, t))
circ₂(cons₂(lift, s), cons₂(lift, t)) -> cons₂(lift, circ₂(s, t))
circ₂(circ₂(s, t), u) -> circ₂(s, circ₂(t, u))
circ₂(s, id) -> s
circ₂(id, s) -> s
circ₂(cons₂(lift, s), circ₂(cons₂(lift, t), u)) -> circ₂(cons₂(lift, circ₂(s, t)), u)
subst₂(a, id) -> a
msubst₂(a, id) -> a
msubst₂(msubst₂(a, s), t) -> msubst₂(a, circ₂(s, t))

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

circ₂(cons₂(a, s), t) -> cons₂(msubst₂(a, t), circ₂(s, t))
circ₂(cons₂(lift, s), cons₂(a, t)) -> cons₂(a, circ₂(s, t))
circ₂(cons₂(lift, s), cons₂(lift, t)) -> cons₂(lift, circ₂(s, t))
circ₂(circ₂(s, t), u) -> circ₂(s, circ₂(t, u))
circ₂(s, id) -> s
circ₂(id, s) -> s
circ₂(cons₂(lift, s), circ₂(cons₂(lift, t), u)) -> circ₂(cons₂(lift, circ₂(s, t)), u)
subst₂(a, id) -> a
msubst₂(a, id) -> a
msubst₂(msubst₂(a, s), t) -> msubst₂(a, circ₂(s, t))

Q is empty.

Using Dependency Pairs [1,13] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

CIRC₂(circ₂(s, t), u) -> CIRC₂(s, circ₂(t, u))
CIRC₂(cons₂(a, s), t) -> MSUBST₂(a, t)
MSUBST₂(msubst₂(a, s), t) -> MSUBST₂(a, circ₂(s, t))
CIRC₂(circ₂(s, t), u) -> CIRC₂(t, u)
CIRC₂(cons₂(lift, s), cons₂(a, t)) -> CIRC₂(s, t)
CIRC₂(cons₂(lift, s), circ₂(cons₂(lift, t), u)) -> CIRC₂(s, t)
CIRC₂(cons₂(a, s), t) -> CIRC₂(s, t)
CIRC₂(cons₂(lift, s), circ₂(cons₂(lift, t), u)) -> CIRC₂(cons₂(lift, circ₂(s, t)), u)
MSUBST₂(msubst₂(a, s), t) -> CIRC₂(s, t)
CIRC₂(cons₂(lift, s), cons₂(lift, t)) -> CIRC₂(s, t)

The TRS R consists of the following rules:

circ₂(cons₂(a, s), t) -> cons₂(msubst₂(a, t), circ₂(s, t))
circ₂(cons₂(lift, s), cons₂(a, t)) -> cons₂(a, circ₂(s, t))
circ₂(cons₂(lift, s), cons₂(lift, t)) -> cons₂(lift, circ₂(s, t))
circ₂(circ₂(s, t), u) -> circ₂(s, circ₂(t, u))
circ₂(s, id) -> s
circ₂(id, s) -> s
circ₂(cons₂(lift, s), circ₂(cons₂(lift, t), u)) -> circ₂(cons₂(lift, circ₂(s, t)), u)
subst₂(a, id) -> a
msubst₂(a, id) -> a
msubst₂(msubst₂(a, s), t) -> msubst₂(a, circ₂(s, t))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

CIRC₂(circ₂(s, t), u) -> CIRC₂(s, circ₂(t, u))
CIRC₂(cons₂(a, s), t) -> MSUBST₂(a, t)
MSUBST₂(msubst₂(a, s), t) -> MSUBST₂(a, circ₂(s, t))
CIRC₂(circ₂(s, t), u) -> CIRC₂(t, u)
CIRC₂(cons₂(lift, s), cons₂(a, t)) -> CIRC₂(s, t)
CIRC₂(cons₂(lift, s), circ₂(cons₂(lift, t), u)) -> CIRC₂(s, t)
CIRC₂(cons₂(a, s), t) -> CIRC₂(s, t)
CIRC₂(cons₂(lift, s), circ₂(cons₂(lift, t), u)) -> CIRC₂(cons₂(lift, circ₂(s, t)), u)
MSUBST₂(msubst₂(a, s), t) -> CIRC₂(s, t)
CIRC₂(cons₂(lift, s), cons₂(lift, t)) -> CIRC₂(s, t)

The TRS R consists of the following rules:

circ₂(cons₂(a, s), t) -> cons₂(msubst₂(a, t), circ₂(s, t))
circ₂(cons₂(lift, s), cons₂(a, t)) -> cons₂(a, circ₂(s, t))
circ₂(cons₂(lift, s), cons₂(lift, t)) -> cons₂(lift, circ₂(s, t))
circ₂(circ₂(s, t), u) -> circ₂(s, circ₂(t, u))
circ₂(s, id) -> s
circ₂(id, s) -> s
circ₂(cons₂(lift, s), circ₂(cons₂(lift, t), u)) -> circ₂(cons₂(lift, circ₂(s, t)), u)
subst₂(a, id) -> a
msubst₂(a, id) -> a
msubst₂(msubst₂(a, s), t) -> msubst₂(a, circ₂(s, t))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

CIRC₂(cons₂(a, s), t) -> MSUBST₂(a, t)
CIRC₂(cons₂(lift, s), cons₂(a, t)) -> CIRC₂(s, t)
CIRC₂(cons₂(lift, s), circ₂(cons₂(lift, t), u)) -> CIRC₂(s, t)
CIRC₂(cons₂(a, s), t) -> CIRC₂(s, t)
CIRC₂(cons₂(lift, s), circ₂(cons₂(lift, t), u)) -> CIRC₂(cons₂(lift, circ₂(s, t)), u)
CIRC₂(cons₂(lift, s), cons₂(lift, t)) -> CIRC₂(s, t)

The remaining pairs can at least be oriented weakly.

CIRC₂(circ₂(s, t), u) -> CIRC₂(s, circ₂(t, u))
MSUBST₂(msubst₂(a, s), t) -> MSUBST₂(a, circ₂(s, t))
CIRC₂(circ₂(s, t), u) -> CIRC₂(t, u)
MSUBST₂(msubst₂(a, s), t) -> CIRC₂(s, t)

Used ordering: Polynomial interpretation [21]:

POL(CIRC₂(x₁, x₂)) = 1 + x₁ + 2·x₁·x₂
POL(MSUBST₂(x₁, x₂)) = 1 + x₁ + x₁·x₂ + x₂
POL(circ₂(x₁, x₂)) = x₁ + 2·x₁·x₂ + x₂
POL(cons₂(x₁, x₂)) = 1 + x₁ + x₂
POL(id) = 2
POL(lift) = 3
POL(msubst₂(x₁, x₂)) = x₁ + 2·x₁·x₂ + 2·x₂

The following usable rules [14] were oriented:

circ₂(cons₂(lift, s), cons₂(a, t)) -> cons₂(a, circ₂(s, t))
circ₂(cons₂(lift, s), circ₂(cons₂(lift, t), u)) -> circ₂(cons₂(lift, circ₂(s, t)), u)
msubst₂(a, id) -> a
circ₂(id, s) -> s
circ₂(cons₂(a, s), t) -> cons₂(msubst₂(a, t), circ₂(s, t))
msubst₂(msubst₂(a, s), t) -> msubst₂(a, circ₂(s, t))
circ₂(s, id) -> s
circ₂(circ₂(s, t), u) -> circ₂(s, circ₂(t, u))
circ₂(cons₂(lift, s), cons₂(lift, t)) -> cons₂(lift, circ₂(s, t))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ QDPOrderProof

        ↳ QDP

          ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

CIRC₂(circ₂(s, t), u) -> CIRC₂(s, circ₂(t, u))
MSUBST₂(msubst₂(a, s), t) -> MSUBST₂(a, circ₂(s, t))
CIRC₂(circ₂(s, t), u) -> CIRC₂(t, u)
MSUBST₂(msubst₂(a, s), t) -> CIRC₂(s, t)

The TRS R consists of the following rules:

circ₂(cons₂(a, s), t) -> cons₂(msubst₂(a, t), circ₂(s, t))
circ₂(cons₂(lift, s), cons₂(a, t)) -> cons₂(a, circ₂(s, t))
circ₂(cons₂(lift, s), cons₂(lift, t)) -> cons₂(lift, circ₂(s, t))
circ₂(circ₂(s, t), u) -> circ₂(s, circ₂(t, u))
circ₂(s, id) -> s
circ₂(id, s) -> s
circ₂(cons₂(lift, s), circ₂(cons₂(lift, t), u)) -> circ₂(cons₂(lift, circ₂(s, t)), u)
subst₂(a, id) -> a
msubst₂(a, id) -> a
msubst₂(msubst₂(a, s), t) -> msubst₂(a, circ₂(s, t))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 2 SCCs with 1 less node.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ QDPOrderProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ QDPOrderProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

CIRC₂(circ₂(s, t), u) -> CIRC₂(s, circ₂(t, u))
CIRC₂(circ₂(s, t), u) -> CIRC₂(t, u)

The TRS R consists of the following rules:

circ₂(cons₂(a, s), t) -> cons₂(msubst₂(a, t), circ₂(s, t))
circ₂(cons₂(lift, s), cons₂(a, t)) -> cons₂(a, circ₂(s, t))
circ₂(cons₂(lift, s), cons₂(lift, t)) -> cons₂(lift, circ₂(s, t))
circ₂(circ₂(s, t), u) -> circ₂(s, circ₂(t, u))
circ₂(s, id) -> s
circ₂(id, s) -> s
circ₂(cons₂(lift, s), circ₂(cons₂(lift, t), u)) -> circ₂(cons₂(lift, circ₂(s, t)), u)
subst₂(a, id) -> a
msubst₂(a, id) -> a
msubst₂(msubst₂(a, s), t) -> msubst₂(a, circ₂(s, t))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

CIRC₂(circ₂(s, t), u) -> CIRC₂(s, circ₂(t, u))
CIRC₂(circ₂(s, t), u) -> CIRC₂(t, u)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [21]:

POL(CIRC₂(x₁, x₂)) = 3·x₁ + 2·x₂
POL(circ₂(x₁, x₂)) = 3 + x₁ + x₂
POL(cons₂(x₁, x₂)) = 1
POL(id) = 0
POL(lift) = 0
POL(msubst₂(x₁, x₂)) = 0

The following usable rules [14] were oriented:

circ₂(s, id) -> s
circ₂(cons₂(lift, s), cons₂(a, t)) -> cons₂(a, circ₂(s, t))
circ₂(cons₂(lift, s), circ₂(cons₂(lift, t), u)) -> circ₂(cons₂(lift, circ₂(s, t)), u)
circ₂(circ₂(s, t), u) -> circ₂(s, circ₂(t, u))
circ₂(id, s) -> s
circ₂(cons₂(lift, s), cons₂(lift, t)) -> cons₂(lift, circ₂(s, t))
circ₂(cons₂(a, s), t) -> cons₂(msubst₂(a, t), circ₂(s, t))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ QDPOrderProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ PisEmptyProof

              ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

circ₂(cons₂(a, s), t) -> cons₂(msubst₂(a, t), circ₂(s, t))
circ₂(cons₂(lift, s), cons₂(a, t)) -> cons₂(a, circ₂(s, t))
circ₂(cons₂(lift, s), cons₂(lift, t)) -> cons₂(lift, circ₂(s, t))
circ₂(circ₂(s, t), u) -> circ₂(s, circ₂(t, u))
circ₂(s, id) -> s
circ₂(id, s) -> s
circ₂(cons₂(lift, s), circ₂(cons₂(lift, t), u)) -> circ₂(cons₂(lift, circ₂(s, t)), u)
subst₂(a, id) -> a
msubst₂(a, id) -> a
msubst₂(msubst₂(a, s), t) -> msubst₂(a, circ₂(s, t))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ QDPOrderProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

MSUBST₂(msubst₂(a, s), t) -> MSUBST₂(a, circ₂(s, t))

The TRS R consists of the following rules:

circ₂(cons₂(a, s), t) -> cons₂(msubst₂(a, t), circ₂(s, t))
circ₂(cons₂(lift, s), cons₂(a, t)) -> cons₂(a, circ₂(s, t))
circ₂(cons₂(lift, s), cons₂(lift, t)) -> cons₂(lift, circ₂(s, t))
circ₂(circ₂(s, t), u) -> circ₂(s, circ₂(t, u))
circ₂(s, id) -> s
circ₂(id, s) -> s
circ₂(cons₂(lift, s), circ₂(cons₂(lift, t), u)) -> circ₂(cons₂(lift, circ₂(s, t)), u)
subst₂(a, id) -> a
msubst₂(a, id) -> a
msubst₂(msubst₂(a, s), t) -> msubst₂(a, circ₂(s, t))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

MSUBST₂(msubst₂(a, s), t) -> MSUBST₂(a, circ₂(s, t))

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [21]:

POL(MSUBST₂(x₁, x₂)) = 3·x₁ + 3·x₁·x₂ + 3·x₂
POL(circ₂(x₁, x₂)) = 1 + 2·x₁ + x₁·x₂ + x₂
POL(cons₂(x₁, x₂)) = 3 + 3·x₂
POL(id) = 3
POL(lift) = 0
POL(msubst₂(x₁, x₂)) = 2 + 2·x₁ + 2·x₁·x₂ + 2·x₂

The following usable rules [14] were oriented:

circ₂(s, id) -> s
circ₂(cons₂(lift, s), cons₂(a, t)) -> cons₂(a, circ₂(s, t))
circ₂(cons₂(lift, s), circ₂(cons₂(lift, t), u)) -> circ₂(cons₂(lift, circ₂(s, t)), u)
circ₂(circ₂(s, t), u) -> circ₂(s, circ₂(t, u))
circ₂(id, s) -> s
circ₂(cons₂(lift, s), cons₂(lift, t)) -> cons₂(lift, circ₂(s, t))
circ₂(cons₂(a, s), t) -> cons₂(msubst₂(a, t), circ₂(s, t))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ QDPOrderProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ PisEmptyProof

Q DP problem:
P is empty.
The TRS R consists of the following rules:

circ₂(cons₂(a, s), t) -> cons₂(msubst₂(a, t), circ₂(s, t))
circ₂(cons₂(lift, s), cons₂(a, t)) -> cons₂(a, circ₂(s, t))
circ₂(cons₂(lift, s), cons₂(lift, t)) -> cons₂(lift, circ₂(s, t))
circ₂(circ₂(s, t), u) -> circ₂(s, circ₂(t, u))
circ₂(s, id) -> s
circ₂(id, s) -> s
circ₂(cons₂(lift, s), circ₂(cons₂(lift, t), u)) -> circ₂(cons₂(lift, circ₂(s, t)), u)
subst₂(a, id) -> a
msubst₂(a, id) -> a
msubst₂(msubst₂(a, s), t) -> msubst₂(a, circ₂(s, t))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.